Inference at * 2 2 2 
Iof proof for Lemma member nth tl:

.....falsecase..... NILNIL

1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. x : T
6. T List
7. u : T
8. v : T List
9. (x  nth_tl(n;v))  (x  v)
10. 0 < n
  (x  nth_tl(n - 1;tl([u / v])))  (x  [u / v]) 

latex

 by ((Reduce 0) 
CollapseTHEN (Auto)) 

latex

C1: 

C1: 11. (x  nth_tl(n - 1;v))
C1:   (x  [u / v])
C.

Definitions	tl(l), [car / cdr], P  Q, type List, a < b, , Type, (x  l), nth_tl(n;as), x:A. B(x), x:AB(x), s = t, n - m, t  T, #$n
Lemmas	l member wf, nth tl wf